\documentclass[xcolor={dvipsnames}]{beamer}

\usepackage{beamerthemesplit}
\usepackage{graphicx}
\usepackage{listings}
\usepackage{pgfgantt}
\usepackage{subcaption}
\usepackage{tikz}
\usetikzlibrary{positioning,shapes,shadows,arrows,backgrounds,fit,decorations.markings}

\beamertemplatenavigationsymbolsempty

\usetheme{Frankfurt}
\useinnertheme{rectangles}

\lstset{
	basicstyle={\ttfamily\scriptsize},
	breakautoindent=true,
	breaklines=true,
	captionpos=b,
	extendedchars=true,
	frame=single,
	numbers=left,
	numberstyle={\tiny},
	showspaces=false,
	showstringspaces=false,
	tabsize=2,
	keywordstyle={\color{MidnightBlue}},
	commentstyle={\color{Aquamarine}},
	literate={~} {$\sim$}{1}
}

\title[Muen Separation Kernel]{Muen - An x86/64 Separation Kernel for\\High Assurance}
\author{Reto Buerki \and Adrian-Ken Rueegsegger}
\institute[HSR]
{
	Institute for Internet Technologies and Applications\\
	University of Applied Sciences Rapperswil
}
\titlegraphic{\includegraphics[scale=0.3]{images/muen.pdf}}

\begin{document}
\input{tikzstyle}

\begin{frame}
	\titlepage
\end{frame}

\section*{Outline}
\begin{frame}
	\frametitle{Outline}\tableofcontents
\end{frame}

\section{Introduction}
\subsection{Background}
\begin{frame}\frametitle{Virtualization}
\begin{itemize}
	\item Virtualization performed by \emph{virtual machine monitor} (VMM)
\end{itemize}

\begin{figure}[h!]
	\centering
	\begin{subfigure}[b]{0.4\textwidth}
		\centering
		\input{graph_vmm_type1}
		\caption{\emph{Type I, native or bare metal VMM.} Runs directly on the
		hardware in the most privileged processor mode.}
	\end{subfigure}
	\qquad
	\begin{subfigure}[b]{0.4\textwidth}
		\centering
		\input{graph_vmm_type2}
		\caption{\emph{Type II or hosted VMM.} The VMM runs on top of a
		conventional operating system and uses OS services.}
	\end{subfigure}
\end{figure}
\end{frame}

\begin{frame}\frametitle{Intel Virtualization Technologies}
\begin{itemize}
	\item VT-x is Intel's technology for virtualization on the x86 platform
	\item Virtual machine state stored in virtual-machine control structure (VMCS)
	\item Virtual-machine extensions (VMX) provide CPU instructions to manage VMCS
	\item VMM runs in VMX root mode
	\item Virtual machines run in VMX non-root mode
	\item Hardware assisted virtualization simplifies implementation of VMM
\end{itemize}
\end{frame}

\begin{frame}\frametitle{SPARK}
\begin{itemize}
	\item Precisely defined programming language based on Ada
	\item Intended for writing high integrity and security software
	\item Program and proof annotations as Ada comments
	\item Allows proof of absence of runtime errors
	\item Allows partial proof of correctness
	\item Industrial usage in Avionics, Space, Medical Systems and Military
\end{itemize}

\lstinputlisting[language=Ada]{lst_spark}
\end{frame}

\begin{frame}\frametitle{Separation Kernel}
\begin{itemize}
	\item Concept introduced by John Rushby (1981)
	\item Partition system into multiple subjects which behave as if they were running on dedicated hardware
	\item Kernel must guarantee component separation
	\item Ideal as basis for a component-based system
	\item No channels for information flow between components other than those explicitly provided
	\item Partitioning and isolation of resources\\(CPU, memory, devices, \textellipsis)
	\item Static configuration during integration
	\item Only includes necessary features $\rightarrow$ small TCB
	\item Well suited for formal verification
\end{itemize}
\end{frame}

\subsection{Motivation}
\begin{frame}\frametitle{Motivation}
\begin{itemize}
	\item Currently available (monolithic) systems unsuitable
	\item Implementation suitable for high assurance systems
	\item Increase confidence in systems built with COTS hardware
	\item Public sources and documentation enable third-party review
	\item Many advances in Intel hardware support for virtualization
\end{itemize}
\end{frame}

\subsection{Goals}
\begin{frame}\frametitle{Goals}
\begin{itemize}
	\item Open-source separation kernel (GPLv3+)
	\item Implementation in SPARK
	\item Proof of absence of runtime errors
	\item Small code size
	\item Reduction to essential functionality
	\item Leverage latest hardware features of Intel platform\\(VT-x, EPT, VT-d, \textellipsis)
	\item Target platform is 64-bit Intel
	\item Only allow intended data flows
	\item Prevent or limit possible side-/covert channels
\end{itemize}
\end{frame}

\section{Implementation}
\subsection{Overview}
\begin{frame}\frametitle{Architecture}
\begin{itemize}
	\item Kernel guarantees subject isolation
	\item Spatial isolation by memory management, VT-x
	\item Temporal isolation by scheduling
\end{itemize}
\begin{center}
	\input{graph_arch_overview}
\end{center}
\end{frame}

\begin{frame}\frametitle{Policy}
\begin{itemize}
	\item Specifies system configuration
	\begin{itemize}
		\item Hardware of target platform
		\item Kernel configuration
		\item Subject configuration
		\item Scheduling plans
	\end{itemize}
	\item skpolicy tool compiles XML to SPARK sources
\end{itemize}
\lstinputlisting[language=xml, linerange={81-86}]{files/example_system.xml.tmpl}
\end{frame}

\subsection{Subsystems}
\begin{frame}\frametitle{Scheduler I}
\begin{itemize}
	\item Fixed cyclic scheduler
	\item Use of VMX preemption timer
\end{itemize}
\begin{center}
	\input{graph_scheduler}
\end{center}
\end{frame}

\begin{frame}\frametitle{Scheduler II}
\begin{itemize}
	\item Major frame consisting of minor frames
	\item Minor frames specify subject and time slice in ticks
	\item Scheduling plan specifies minor frames per logical CPU
	\item $\tau$0 subject can switch scheduling plan
\end{itemize}

\begin{center}
	\noindent\resizebox{\textwidth}{!}{\input{graph_major_frame}}
\end{center}
\end{frame}

\begin{frame}[fragile]\frametitle{Scheduler III}
\begin{lstlisting}[language=xml]
<major_frame>
    <cpu>
        <minor_frame subject_id="0" ticks="200"/>
    </cpu>
    <cpu>
        <minor_frame subject_id="1" ticks="40"/>
        <minor_frame subject_id="2" ticks="80"/>
        <minor_frame subject_id="1" ticks="40"/>
        <minor_frame subject_id="2" ticks="40"/>
    </cpu>
</major_frame>
\end{lstlisting}

\begin{center}
	\noindent\resizebox{\textwidth}{!}{\input{graph_scheduling_plan}}
\end{center}
\end{frame}

\begin{frame}\frametitle{Traps}
\begin{itemize}
	\item Transition to VMX root mode is called a trap
	\item Policy specifies per-subject trap table
	\item Trap causes subject handover according to policy
	\item Trap may inject interrupt in destination subject
	\item Reserved traps are handled differently
		\begin{itemize}
			\item VMX preemption timer
			\item External interrupt
			\item Interrupt window
			\item Hypercall
		\end{itemize}
	\item Virtualization using "Trap and Emulate"
\end{itemize}
\lstinputlisting[language=xml]{lst_trap_table}
\end{frame}

\begin{frame}\frametitle{External Interrupts}
\begin{itemize}
	\item Policy assigns devices to subjects
	\item Setup of interrupt routing according to policy
\end{itemize}
\begin{center}
	\noindent\resizebox{.55\textwidth}{!}{\input{graph_external_interrupt}}
\end{center}
\begin{enumerate}
	\item External interrupts cause traps on designated CPU
	\item Kernel adds pending event to destination subject
	\item Pending events are injected on resumption of subject
	\item Subject handles injected event as interrupt
\end{enumerate}
\end{frame}

\begin{frame}\frametitle{Event Handling}
\begin{itemize}
	\item Event is a hypercall triggered by subject using VMCALL instruction
	\item Policy specifies per-subject event table
	\item Handover events transfers execution to destination subject optionally injecting an interrupt
	\item Interrupt events inject interrupt in destination subject with optional IPI
\end{itemize}
\lstinputlisting[language=xml]{lst_event_table}
\end{frame}

\begin{frame}\frametitle{Multicore}
\begin{itemize}
	\item Kernel starts on bootstrap processor (BSP)
	\item BSP starts application processors (APs)
	\item All CPUs synchronize on major frame changes
\end{itemize}
\begin{center}
	\input{graph_mp_overview}
\end{center}
\end{frame}

\begin{frame}\frametitle{Inter-Core Events}
\begin{center}
	\input{graph_events}
\end{center}
\end{frame}

\begin{frame}\frametitle{Demo}
\begin{itemize}
	\item Untrusted VM subject running MIT's xv6 OS
	\item Native VT subject provides virtual terminals and keyboard
	\item Native subject monitor (SM) observes xv6 subject
	\begin{itemize}
		\item Emulates port I/O
		\item Halts xv6 on invalid operation
	\end{itemize}
	\item Native crypter provides hashing service
	\begin{itemize}
		\item Inter-subject communication using shared memory pages
		\item Signalisation using event mechanism
	\end{itemize}
\end{itemize}
\begin{center}
	\input{graph_arch_example}
\end{center}
\end{frame}

\section{Analysis}
\subsection{Separation}
\begin{frame}\frametitle{VMX Controls - Exiting}

\begin{small}
\begin{table}[h]
	\centering
	\begin{tabular}{l|c|c}
		\textbf{Event} & \textbf{Native} & \textbf{VM} \\
		\hline
		External interrupt          & \checkmark & \checkmark  \\
		VMX preemption timer        & \checkmark & \checkmark  \\
		Execute \texttt{INVLPG}	    & \checkmark & \checkmark \\
		Execute \texttt{MONITOR}    & \checkmark & \checkmark \\
		Execute \texttt{MWAIT}      & \checkmark & \checkmark \\
		Execute \texttt{RDPMC}      & \checkmark & \checkmark \\
		Execute \texttt{RDTSC}      & \checkmark & \checkmark \\
		Execute \texttt{WBINVD}     & \checkmark & \checkmark \\
		MOV to CR3                  & \checkmark & \\
		MOV from CR3                & \checkmark & \\
		MOV to CR8                  & \checkmark & \checkmark \\
		MOV from CR8                & \checkmark & \checkmark \\
		MOV to/from debug registers & \checkmark & \checkmark \\
		\hline
		I/O port access & \checkmark & \checkmark \\
		MSR access      & \checkmark & \checkmark \\
		Exceptions      & \checkmark & \\
	\end{tabular}
\end{table}
\end{small}
\end{frame}

\begin{frame}\frametitle{System Resources}
\begin{itemize}
	\item Assigned to subjects according to policy
	\item Assignment is static at integration time
\end{itemize}
\begin{block}{Memory}
	\begin{itemize}
		\item Specified by memory regions in kernel/subjects spec
		\item Policy compiler creates page tables
	\end{itemize}
\end{block}

\begin{block}{Devices}
	\begin{itemize}
		\item Assignment to subject grants resources\\(memory, ports, interrupts)
		\item Policy compiler
		\begin{itemize}
			\item Maps memory regions into subject's address space
			\item Enables I/O port access via VMCS I/O bitmap
			\item Creates interrupt routing table entry
		\end{itemize}
	\end{itemize}
\end{block}
\end{frame}

\begin{frame}\frametitle{Execution Environment}
\begin{footnotesize}
\begin{table}[h]
	\centering
	\begin{tabular}{l|c|c|c}
		\textbf{Component} & \textbf{VMCS} & \textbf{State} & \textbf{Denied} \\
		\hline
		General purpose registers  & & \checkmark \\
		Segment registers          & \checkmark & \\
		Instruction pointer        & \checkmark & \\
		Flag register              & \checkmark & \\
		CR0                        & \checkmark & \\
		CR2                        & & \checkmark \\
		CR3                        & \checkmark & \\
		CR4                        & \checkmark & \\
		CR8                        & & & \checkmark \\
		Descriptor table registers & \checkmark & \\
		DR0-3                      & & & \checkmark \\
		DR6                        & & & \checkmark \\
		DR7                        & & & \checkmark \\
		x87 FPU registers          & & & \checkmark \\
		MMX registers              & & & \checkmark \\
		XMM registers              & & & \checkmark \\
		MSRs                       & & & (\checkmark) \\
	\end{tabular}
\end{table}
\end{footnotesize}
\end{frame}

\begin{frame}\frametitle{Temporal Isolation}
\begin{itemize}
	\item Fixed cyclic scheduler
	\item Static scheduling plan generated from policy
	\item Subject preemption using VMX preemption timer
	\item Sum of minor frame lengths per CPU/major frame are equal
	\item Global barrier sync at beginning of major frame
\end{itemize}
\end{frame}

\section{Conclusion}
\subsection{Results}
\begin{frame}\frametitle{Results}
\begin{itemize}
	\item Minimal Zero-Footprint Run-Time (RTS)
	\item Kernel
	\item Tools
	\begin{itemize}
		\item Policy compilation tool (\texttt{skpolicy})
		\item Config generation tool (\texttt{skconfig})
		\item Packaging tool (\texttt{skpacker})
	\end{itemize}
	\item Subjects
	\begin{itemize}
		\item Initial $\tau$0 implementation
		\item Virtual terminals \& keyboard
		\item xv6 OS with minimal adjustments
		\item Subject monitor for xv6
		\item Crypter
		\item Dumper
	\end{itemize}
	\item Documentation
\end{itemize}
\end{frame}

\begin{frame}\frametitle{Results - Kernel}
\begin{itemize}
	\item Source code statistics:
	\begin{itemize}
		\item $\sim$260 lines of Assembly
		\item $\sim$2470 lines of SPARK
	\end{itemize}§
	\item Proof of absence of runtime errors (All VCs discharged)
	\item Static assignment of resources according to policy
	\item Multicore support
	\item EPT and memory typing (PAT)
	\item Event mechanism
	\item Support for native 64-bit subjects
	\item Support for VM subjects
\end{itemize}
\end{frame}

\subsection{Future Work}
\begin{frame}\frametitle{Future Work}
\begin{block}{Mid-term}
	\begin{itemize}
		\item Linux virtualization
		\item Hardware passthrough/PCIe virtualization
		\item Extend $\tau$0
		\item Covert/Side-Channel analysis
	\end{itemize}
\end{block}
\begin{block}{Long-term}
	\begin{itemize}
		\item MP subjects
		\item Fully virtualized subjects (Windows)
		\item Power Management
		\item Performance optimization
		\item Formal verification
	\end{itemize}
\end{block}
\end{frame}

\subsection{Questions}
\begin{frame}\frametitle{Questions?}
\begin{center}
	Thank you for your attention!
\end{center}
\end{frame}

\end{document}
